COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro.tex[let,jmc]
C00020 00003	Ma Xiwen's axioms for Mr. S and Mr. P which are a variant of an
C00022 00004	DECLARE INDVAR t ε NATNUM
C00025 00005	# LEMMA 1
C00026 00006
C00027 ENDMK
C⊗;
\input macro.tex[let,jmc]
\ctrline{\bf FORMALIZATION OF TWO PUZZLES INVOLVING KNOWLEDGE}
\yyskip

	This paper describes a formal system and uses it to
express the puzzle of the three wise men and the puzzle of Mr. S
and Mr. P.  Four innovations in the axiomatization of knowledge
were required: the ability to express joint knowledge of several
people, the ability to express the initial non-knowledge,
the ability to describe knowing what rather than merely knowing that,
and the ability to express the change which occurs when someone
learns something.  Our axioms are written in first order logic
and use Kripke-style possible worlds directly rather than modal
operators or imitations thereof.  We intend to use functions
imitating modal operators and taking "propositions" and "individual
concepts" as operands, but we haven't yet solved the problem
of how to treat learning in such a formalism.

	The puzzles to be treated are the following:

\noindent {\bf The three wise men}

	{\it ``A certain king wishes to test his three wise men.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then repeatedly asks them, ``Do you know the cclor of
your spot".  What do they answer?''}

	The solution is that they answer, {\it ``No''}, the first two
times the question is asked and answer {\it ``Yes''} thereafter.

	This is a variant form of the puzzle.  The traditional form
is

	{\it ``A certain king wishes to determine which of his three
wise men is the wisest.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then offers his favor to the one who will first tell
him the color of his spot.  After a while, the wisest announces
that his spot his white.  How does he know?''}

	The intended solution is that the wisest reasons that if
his spot were black, the second would see a black and a white and
would reason that if his spot were black, the third would have seen
two black spot and reasoned from the king's announcement that his
spot was white.  This traditional version  requires
the wise men to reason about how fast their colleagues reason, and
we don't wish to try to formalize this.

\noindent {\bf Mr. S and Mr. P}

	{\it Two numbers $m$ and $n$ are chosen such that $2 ≤ m ≤ n ≤ 99$.
Mr. S is told their sum and Mr. P is told their product.  The following
dialogue ensues:}

\halign {\it Mr. P:	I don't know the numbers.\cr 
Mr. S:	I knew you didn't know.  I don't know either.\cr 

Mr. P:	Now I know the numbers.\cr 

Mr. S:	Now I know them too.\cr 

In view of the above dialogue, what are the numbers?\cr}

\yyskip
\noindent {\bf Simple axiomatization of the wise men}

	If we can assume that the first and second wisemen don't
know the colors of their spots, that the second knows that the
first doesn't know, and the third knows this, then a simple
axiomatization that doesn't explicitly treat learning works.

[In this draft, we omit this section.  Instead we include an
older self-contained memo written when this was our main approach
to the problem].

\yyskip
\noindent {\bf Full axiomatization of the wise men}

	The axioms are given in a form acceptable to FOL, the proof
checker computer program for an extended first order logic at the
Stanford Artificial Intelligence Laboratory.  FOL uses a sorted
logic and constants and variables are declared to have given sorts,
and quantifiers on these variables are interpreted as ranging over
the sorts corresponding to the variables.

	The axiomatization has the following features:

	\a . It is entirely in first order logic rather than in a modal
logic.

	\a . The Kripke accessibility relation is axiomatized.  No knowledge
operator or function is used.  We hope to present a second axiomatization
using a knowledge function, but we haven't yet decided how to handle time
and learning in such an axiomatization.

	\a . We are essentially treating ``knowing what'' rather than ``knowing
that''.  We say that p knows the color of his spot in world $w$ by saying
that in all worlds accessible from $w$, the color of the spot is the same
as in $w$.

	\a . We treat learning by giving the accessibility relation a time
parameter.  To say that someone learns something is done by saying that
the worlds accessible to him at time $n+1$ are the subset of those accessible
at time $n$ in which the something is true.

	\a . The problems treated are complicated by the need to treat
joint knowledge and joint learning.  This is done by introducing
fictitious persons who know what a group of people know jointly.

\yyskip

$$declare INDCONST RW ε WORLD;$$

declare INDVAR w w1 w2 w3 w4 w5 $ε$ WORLD;

\yskip
	$RW$ denotes the real world, and $w, w1, \ldots , w5$ are variables
ranging over worlds.

declare INDVAR m n m1 m2 m3 n1 n2 n3 $ε$ NATNUM;

	We use natural numbers for times.

\yskip

declare INDCONST S1 S2 S3 S123 $ε$ PERSON;

declare INDVAR p p0 p1 p2 $ε$ PERSON;

\yskip
	$S1$, $S2$ and $S3$ are the three wisemen.  $S123$
 is a fictitious person
who knows whatever $S1$, $S2$ and $S3$ know jointly.
  The joint knowledge of several
people is typified by events that occur in their joint presence.  Not only do
they all know it, but $S1$ knows that $S2$ knows that $S1$ knows that $S3$
 knows etc.
Instead of introducing $S123$, we could introduce prefixes of like ``$S1$
knows that $S2$ knows'' as objects and quantify over prefixes.

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

	This Kripke-style accessibility relation has two more arguments than
is usual in modal logic - a person and a time.

\yskip
declare INDVAR c c1 c2 c3 c4 $ε$ COLORS;

declare INDCONST W B $ε$ COLORS;

	There are two colors - white and black.

declare OPCONST color(PERSON,WORLD) = COLORS;

	A person has a color in a world.  Note that the previous
axiomatization was simpler.  We merely had three propositions WISE1, WISE2
and WISE3 asserting that the respective wise men had white spots.  We need
the colors, because we want to quantify over colors.

axiom reflex:	$∀w p m.A(w,w,p,m)$;;

	The accessibility relation is reflexive as is usual in the Kripke
semantics of M.

axiom transitive:	$∀w1 w2 w3 p m.(A(w1,w2,p,m)
 ∧ A(w2,w3,p,m) ⊃ A(w1,w3,p,m));;$

	Making the accessibility relation transitive gives an S4 like system.
We use transitivity in the proof, but we aren't sure it is necessary.

axiom who:	$∀p.(p=S1 ∨ p=S2 ∨ p=S3 ∨ p=S123);;$

	We need to delimit the set of wise men.

axiom w123:	$∀w1 w2 m.(A(w1,w2,S1,m) ∨ A(w1,w2,S2,m) ∨ A(w1,w2,S3,m)
⊃ A(w1,w2,S123,m));;$

	This says that anything the wise men know jointly, they
know individually.

axiom foolspot:	$∀w.(color(S123,w)=W);;$

	This ad hoc axiom is the penalty for introducing $S123$ as an
ordinary individual whose spot must therefore have a color.  It would have
been better to distinguish between real persons with spots and the
fictitious person(s) who only know things.  Anyway, we give $S123$ a white
spot and make it generally known, e.g. true in all possible worlds.


axiom color:	$¬(W=B)$

		$∀c.(c=W ∨ c=B)$

;;

	Both of these axioms about the colors are used in the proof.

axiom rw:	$color(S1,RW) = W ∧ color(S2,RW) = W ∧ color(S3,RW) = W;;$

	In fact all spots are white.

axiom king:	$∀w.(A(RW,w,S123,0) ⊃ color(S1,w)=W ∨ color(S2,w)=W
∨ color(S3,w)=W);;$

	They jointly know that at least one spot is white, since
the king stated it in their mutual presence.  We use the consequence
that S3 knows that S2 knows that S1 knows this fact.


axiom initial:	$∀c w.(A(RW,w,S123,0) ⊃
	(c=W ∨ color(S2,w)=W ∨ color(S3,w)=W
		⊃ ∃w1.(A(w,w1,S1,0) ∧ color(S1,w1) = c)) ∧
	(c=W ∨ color(S1,w)=W ∨ color(S3,w)=W
		⊃ ∃w1.(A(w,w1,S2,0) ∧ color(S2,w1) = c)) ∧
	(c=W ∨ color(S1,w)=W ∨ color(S2,w)=W
		⊃ ∃w1.(A(w,w1,S3,0) ∧ color(S3,w1) = c)))$

	$∀w w1.(A(RW,w,S123,0) ∧ A(w,w1,S1,0)
⊃ color(S2,w1) = color(S2,w) ∧ color(S3,w1) = color(S3,w))$

	$∀w w1.(A(RW,w,S123,0) ∧ A(w,w1,S2,0)
⊃ color(S1,w1) = color(S1,w) ∧ color(S3,w1) = color(S3,w))$

	$∀w w1.(A(RW,w,S123,0) ∧ A(w,w1,S3,0)
 color(S1,w1) = color(S1,w) ∧ color(S2,w1) = color(S2,w))$
;;

	These are actually four axioms.  The last three say that every one
knows that each knows the colors of the other men's spots.
The first part says that they all know that no-one knows anything
more than what he can see and what the king told them.  We establish
non-knowledge by asserting the existence of enough possible worlds.
The ability to quantify over colors is convenient for expressing this axiom
in a natural way.  In the S and P problem it is essential, because
we would otherwise need a conjunction of 4753 terms.

axiom elwek1:	$∀w.(A(RW,w,S123,1) ≡ A(RW,w,S123,0) ∧
∀p.(∀w1.(A(w,w1,p,0) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,0)
⊃ color(p,w1)=color(p,RW))))$

	$∀w1 w2.(A(w1,w2,S1,1) ≡ A(w1,w2,S1,0) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S2,1) ≡ A(w1,w2,S2,0) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S3,1) ≡ A(w1,w2,S3,0) ∧ A(w1,w2,S123,1))$
;;

	This axiom and the next one are the same except that one
deals with the transition from time $0$ to time $1$ and the other deals
with the transition from time $1$ to time $2$.
Each says that
they jointly learn who (if anyone) knows the color of his spot.  The
quantifier $∀p$ in this axiom covers $S123$ also and forced us to say
that they jointly know the color of $S123$'s spot.

axiom elwek2:	$∀w.(A(RW,w,S123,2) ≡ A(RW,w,S123,1) ∧
∀p.(∀w1.(A(w,w1,p,1) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,1)
⊃ color(p,w1)=color(p,RW))))$

	$∀w1 w2.(A(w1,w2,S1,2) ≡ A(w1,w2,S1,1) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S2,2) ≡ A(w1,w2,S2,1) ∧ A(w1,w2,S123,1))$

	$∀w1 w2.(A(w1,w2,S3,2) ≡ A(w1,w2,S3,1) ∧ A(w1,w2,S123,1))$
;;

	The file WISEMA.PRF[S78,JMC] at the Stanford AI Lab contains
a computer checked proof from these axioms of

$$∀w.(A(RW,w,S3,2) ⊃ color(S3,w) = color(S3,RW))$$

which is the assertion that at time $2$, the third wise man knows the
color of his spot.  As intermediate results we had to prove that
previous to time $2$, the other wise men did not know the colors of
their spots.  In this symmetrical axiomatization, we could have proved
the theorem with a variable wise man instead of the constant $S3$.


\noindent {\bf Axiomatization of Mr. S and Mr. P}

	These axioms involve the same ideas as the second wise man
axiomatization.  In fact, we derived them first.  The following modified
version of some axioms by Ma Xiwen of Peking University separates the
knowledge part of the problem from the arithmetic
part in a neat way.

Ma Xiwen's axioms for Mr. S and Mr. P which are a variant of an
earlier version by McCarthy.

 	 This is an approach to the axiomatization of Mr.S and Mr.P.
      	Its basic idea is the same of KNOW[E78,JMC].                  
	 These are some diffrent symbols:
 
		k	for a PAIR of NATNUMs
		s(k)    for the sum of the two NATNUM in k
		p(k)    for the product of the two NATNUM in k
	
	 We have introduced a few of PREDCONSTs, for abbreviation only.
    	 But there are some important differences between the two 
	axiomatizations: our axiom SP is weaker, but our axioms LP
	and LS are stronger.
 	 The PREDCONSTs R1 R2 and R3 are slightly different,too.
	
	 Next follws a complete list of commands of the FOL proof of
	R3(k0). The subsequent proof that k0=<4,13> will be purely
	arithmetic, and a computer search has been done to confirm
	it.

	 


I have changed the learning axioms LP and LS, and I have removed
the redundant predicate OK.  Where I have times 1 and 2 in
A(RW,w,SP,n), Ma had 0.  I think these axioms are too strong and
may even make the system inconsistent.  I don't know whether Ma's
proof will work with the weaker axioms.  - JMC
DECLARE INDVAR t ε NATNUM;
DECLARE INDCONST k0 ε PAIR;
DECLARE INDVAR k k1 k2 k3 ε PAIR;
DECLARE INDCONST RW ε WORLD;
DECLARE INDVAR w w1 w2 w3 ε WORLD;
DECLARE INDCONST S P SP ε PERSON;
DECLARE INDVAR r ε PERSON;
DECLARE OPCONST K(WORLD)=PAIR;  
DECLARE OPCONST s(PAIR)=NATNUM;
DECLARE OPCONST p(PAIR)=NATNUM;
DECLARE PREDCONST A(WORLD,WORLD,PERSON,NATNUM);
DECLARE PREDCONST Qs(PAIR) Qp(PAIR) Q1(PAIR) Q2(PAIR) Q3(PAIR);
DECLARE PREDCONST Bs(WORLD) Bp(WORLD) B1(WORLD) B2(WORLD);
DECLARE PREDCONST R1(PAIR) R2(PAIR) R3(PAIR);
DECLARE PREDCONST C1(WORLD) C2(WORLD);

AXIOM AR: ∀w r t.A(w,w,r,t);;
AXIOM AT: ∀w1 w2 w3 r t.(A(w1,w2,r,t)∧A(w2,w3,r,t)⊃A(w1,w3,r,t));;
AXIOM SP: ∀w1 w2 t.(A(w1,w2,S,t)∨A(w1,w2,P,t)⊃A(w1,w2,SP,t));;
AXIOM RW: k0=K(RW);;
AXIOM INIT:
    	∀w w1.(A(RW,w,SP,0)∧A(w,w1,S,0)⊃s(K(w))=s(K(w1))),
	∀w w1.(A(RW,w,SP,0)∧A(w,w1,P,0)⊃p(K(w))=p(K(w1))),
    	∀w k.(A(RW,w,SP,0)∧s(K(w))=s(k)⊃∃w1.(A(w,w1,S,0)∧k=K(w1))),
	∀w k.(A(RW,w,SP,0)∧p(K(w))=p(k)⊃∃w1.(A(w,w1,P,0)∧k=K(w1)));;

AXIOM R:
	∀k.(R1(k)≡Qs(k)∧Q1(k)),
	∀k.(R2(k)≡R1(k)∧Q2(k)),
	∀k.(R3(k)≡R2(k)∧Q3(k));;
AXIOM BS: ∀w.(Bs(w)≡∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))));;
AXIOM BP: ∀w.(Bp(w)≡∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1))));;
AXIOM B:
	∀w.(B1(w)≡∀w1.(A(w,w1,S,0)⊃Bp(w1))),
	∀w.(B2(w)≡∀w1.(A(w,w1,P,1)⊃K(w)=K(w1)));;
AXIOM C:
	∀w.(C1(w)≡Bs(w)∧B1(w)),
	∀w.(C2(w)≡C1(w)∧B2(w));;
AXIOM SKNPK: B1(RW);;
AXIOM NSK:   Bs(RW);;
AXIOM PK:    B2(RW);;
AXIOM SK:    ∀w.(A(RW,w,S,2)⊃K(RW)=K(w));;
AXIOM LP: ∀w w1.(A(RW,w,SP,1)⊃(A(w,w1,P,1)≡A(w,w1,P,0)∧C1(w1)));;
AXIOM LS: ∀w w1.(A(RW,w,SP,2)⊃(A(w,w1,S,2)≡A(w,w1,S,1)∧C2(w1)));;

AXIOM QS: ∀k.(Qs(k)≡∃k1.(s(k)=s(k1)∧¬(k=k1)));;
AXIOM QP: ∀k.(Qp(k)≡∃k1.(p(k)=p(k1)∧¬(k=k1)));;
AXIOM Q:
	∀k.(Q1(k)≡∀k1.(s(k)=s(k1)⊃Qp(k1))),
	∀k.(Q2(k)≡∀k1.(R1(k1)∧p(k)=p(k1)⊃k=k1)),
	∀k.(Q3(k)≡∀k1.(R2(k1)∧s(k)=s(k1)⊃k=k1));;

COMMENT # LEMMA 1
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(Qs(k)≡Bs(w))) 
COMMENT # LEMMA 2
        ∀w k.(A(RW,w,SP,0)∧k=K(w)→(Qp(k)≡Bp(w)))
COMMENT # LEMMA 3
	∀w k.(A(RW.w.SP,0)∧k=K(w)→(Q1(k)≡B1(w)))
COMMENT # LEMMA 4
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R1(k)≡C1(w)))
COMMENT # LEMMA 5
	R2(k0)
COMMENT # LEMMA 6
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R2(k)⊃C2(w)))
COMMENT # LEMMA 7
      	Q3(k0)
COMMENT # MAIN THEOREM
	R3(k0)

\yyskip
John McCarthy

Artificial Intelligence Laboratory

Computer Science Department

Stanford University

Stanford, California 94305

ARPANET: MCCARTHY@SU-AI

This file is KNOW.2[W81,JMC].

\vfill\end